$\forall$$T$:Type, $f$:($\mathbb{N}\rightarrow$($T$ List)), $t$, ${\it t'}$:$\mathbb{N}$.
\\[0ex]$t$$<$${\it t'}$ $\Rightarrow$ concat(map($f$;upto($t$))) @ ($f$($t$)) $\leq$ concat(map($f$;upto(${\it t'}$)))